enrich
   apersistence-base
, 
   index-base
with
   

   
   constants  GROUP_NODE_HEADER_SIZE : nat;
   functions  . .keys : nat-set → key-set;
              . .keys : node-list → key-list;
              . .inos : node-index → nat-set;
              . .lebs : node-index → nat-set;
              . .lebs : address-list → nat-set;
              . .lebs : address-set → nat-set;
              referenced-adrs : address-list × node-index → address-list;
              . .flashsize : node → nat;
              . .flashsize : node-list → nat;
              . .nds : group-node-list → node-list;
   predicates  valid-journal-head : nat-list × group-store × nat-set;
               key-cons : key-list × address-list × group-store × nat-set;
               nodes-cons : address-list × node-list × group-store × nat-set;
               key-cons : node-list;
               transaction : node-list × group-node-list;
               transaction-prefix : node-list × group-node-list;
   
   variables  φ : group-node-list → bool;
   
   

   

   axioms valid-journal-head
          : ⊦   valid-journal-head(nx, gstore, ginval)
              ↔ nx ≠ [] ∧ nx.last ∈ gstore ∧ ¬ nx.last ∈ ginval ∧ (gstore[nx.last].gndlist = [] ∨ gstore[nx.last].gndlist.last.end);
          used for: ls;
          keys-base :  ⊦ ∅.keys = ∅;
          used for: s, ls;
          keys-rec :  ⊦ ¬ n ∈ ns → (ns ++ n).keys = ns.keys ++ inodekey(n);
          used for: s, ls;
          lebs-index :  ⊦ n ∈ ri.lebs ↔ (∃ adr. adr.lnum = n ∧ adr ∈ ri);
          used for: s, ls;
          lebs-base :  ⊦ [].lebs = ∅;
          used for: s, ls;
          lebs-rec :  ⊦ (adr ' + ax).lebs = ax.lebs ++ adr.lnum;
          used for: s, ls;
          lebs-set :  ⊦ n ∈ as.lebs ↔ (∃ adr. adr.lnum = n ∧ adr ∈ as);
          used for: ls;
          inos-node-store-def :  ⊦ n ∈ ri.inos ↔ inodekey(n) ∈ ri;
          used for: s, ls;
          transaction
          : ⊦   transaction(ndx, gndx)
              ↔   # gndx = # ndx
                ∧ (  gndx = []
                   ∨   gndx.head.start ∧ gndx.last.end
                     ∧ (∀ n. (0 < n ∧ n < # gndx → ¬ gndx[n].start) ∧ (n + 1 < # gndx → ¬ gndx[n].end)))
                ∧ (∀ n. n < # gndx → gndx[n].nd = ndx[n]);
          used for: ls;
          transaction-prefix
          : ⊦   transaction-prefix(ndx, gndx)
              ↔   # gndx < # ndx
                ∧ (gndx = [] ∨ gndx.head.start ∧ (∀ n. (0 < n ∧ n < # gndx → ¬ gndx[n].start) ∧ (n < # gndx → ¬ gndx[n].end)))
                ∧ (∀ n. n < # gndx → gndx[n].nd = ndx[n]);
          used for: ls;
          referenced-adrs-base :  ⊦ referenced-adrs([], ri) = [];
          used for: s, ls;
          referenced-adrs-rec :  ⊦ referenced-adrs(adr ' + ax, ri) = (adr ∈ ri ⊃ adr ';[]) + referenced-adrs(ax, ri);
          used for: ls;
          flashsize-node :  ⊦ gnd.flashsize = GROUP_NODE_HEADER_SIZE + nd.flashsize;
          flashsize-nodes-base :  ⊦ [].flashsize = 0;
          used for: s, ls;
          flashsize-nodes-rec :  ⊦ (nd ' + ndx).flashsize = nd.flashsize + ndx.flashsize;
          used for: s, ls;
          keys-base :  ⊦ [].keys = [];
          used for: s, ls;
          keys-rec :  ⊦ (nd ' + ndx).keys = nd.key + ndx.keys;
          used for: s, ls;
          key-cons
          : ⊦   key-cons(kx, ax, gstore, ginval)
              ↔ # kx = # ax ∧ (∀ n. n < # kx → ax[n] ∈ gstore ∧ ¬ ax[n].lnum ∈ ginval ∧ key-cons(kx[n], gstore[ax[n]].nd));
          key-cons-base :  ⊦ key-cons([]);
          used for: s, ls;
          key-cons-rec :  ⊦ key-cons(nd ' + ndx) ↔ ¬ ¬(key-cons(nd.key, nd) ∧ key-cons(ndx));
          used for: s, ls;
          nodes-cons
          : ⊦   nodes-cons(ax, ndx, gstore, ginval)
              ↔ # ax = # ndx ∧ (∀ n. n < # ax → ax[n] ∈ gstore ∧ ¬ ax[n].lnum ∈ ginval ∧ gstore[ax[n]].nd = ndx[n]);
          used for: ls;
          nds-base :  ⊦ [].nds = [];
          used for: s, ls;
          nds-rec :  ⊦ (gnd ' + gndx).nds = gnd.nd + gndx.nds;
          used for: s, ls;

   

   
end enrich